g:OMon, a, b:|g|. (a < b)  ((a  b) & ((b  a))) 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, gset, OMon, goset, a  b, a < b
Definitions	t  T, x:A. B(x), t.2, t.1, , gset, Mon, AbMon, goset, a  b, |p|, OMon, a  b, a < b
Lemmas	omon wf, oset of ocmon wf0, set lt is sp of leq a